The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
foldr#3(Cons(x16, x6)) →⁺ step_x_f(rev_l, x16, foldr#3(x6))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [x6 / Cons(x16, x6)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)